x,y:. decidable((x = y)) 

latex

Definitions	x:A. B(x), , decidable(P), t  T, P  Q, A, sq_type(T), P  Q, guard(T), prop{i:l}, T, True, A  B, False
Lemmas	decidable int equal, not wf, le wf, nat wf